1. $A$ : Type
\\[0ex]2. $B$ : Type
\\[0ex]3. $f$ : $A$$\rightarrow$$B$
\\[0ex]4. $\forall$$a_{1}$, $a_{2}$:$A$. ($f$($a_{1}$) = $f$($a_{2}$)) $\Rightarrow$ ($a_{1}$ = $a_{2}$)
\\[0ex]5. $g$ : $B$$\rightarrow$$A$
\\[0ex]6. $\forall$$b$:$B$. $f$($g$($b$)) = $b$
\\[0ex]$\vdash$  InvFuns($A$;$B$;$f$;$g$)